(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
merge(@l1, @l2) → merge#1(@l1, @l2)
merge#1(::(@x, @xs), @l2) → merge#2(@l2, @x, @xs)
merge#1(nil, @l2) → @l2
merge#2(::(@y, @ys), @x, @xs) → merge#3(#less(@x, @y), @x, @xs, @y, @ys)
merge#2(nil, @x, @xs) → ::(@x, @xs)
merge#3(#false, @x, @xs, @y, @ys) → ::(@y, merge(::(@x, @xs), @ys))
merge#3(#true, @x, @xs, @y, @ys) → ::(@x, merge(@xs, ::(@y, @ys)))
mergesort(@l) → mergesort#1(@l)
mergesort#1(::(@x1, @xs)) → mergesort#2(@xs, @x1)
mergesort#1(nil) → nil
mergesort#2(::(@x2, @xs'), @x1) → mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
mergesort#2(nil, @x1) → ::(@x1, nil)
mergesort#3(tuple#2(@l1, @l2)) → merge(mergesort(@l1), mergesort(@l2))
msplit(@l) → msplit#1(@l)
msplit#1(::(@x1, @xs)) → msplit#2(@xs, @x1)
msplit#1(nil) → tuple#2(nil, nil)
msplit#2(::(@x2, @xs'), @x1) → msplit#3(msplit(@xs'), @x1, @x2)
msplit#2(nil, @x1) → tuple#2(::(@x1, nil), nil)
msplit#3(tuple#2(@l1, @l2), @x1, @x2) → tuple#2(::(@x1, @l1), ::(@x2, @l2))
The (relative) TRS S consists of the following rules:
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
merge(::(#0, @xs5458_4), ::(#0, @ys5520_4)) →+ ::(#0, merge(::(#0, @xs5458_4), @ys5520_4))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@ys5520_4 / ::(#0, @ys5520_4)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)